COMMENT ⊗   VALID 00011 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 00003	.bb "#. Recursive Programs."
C00010 00004	.bb "#. The Functional Equation of a Recursive Program."
C00015 00005	.bb "#. First Order Axioms for Lisp."
C00022 00006	.bb "#. The Minimization Schema."
C00028 00007	.bb "#. Proof Methods as Axiom Schemata"
C00032 00008	.bb "#. Representations Using Finite Approximations."
C00041 00009	.BB "#. Questions of Incompleteness."
C00048 00010	.bb "#. References."
C00051 00011	.skip 1
C00052 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.every heading (REPRESENTATION,...draft...,{page})
.cb REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC


	This paper presents methods of representing recursive programs by
sentences and schemata of first order logic, characterization of
%2recursion induction%1, %2subgoal induction%1, %2inductive assertions%1
and other ways of proving facts about programs as axiom schemata of first
order logic, and applications of these results to proving assertions about
programs.


.bb "#. Introduction and Motivation."

	It has been concluded from the undecideability of both equivalence
and non-equivalence of abstract recursive program schemata that recursive
programs cannot be characterized in first order logic.  Cooper (1969)
showed how to characterize them in second order logic, and that seemed to
settle the matter.  However, we will exhibit first order characterizations
that are incomplete only in that they admit non-standard models like those
of first order arithmetic.  It now seems likely that all "ordinary"
assertions about programs will be provable or disprovable in first order
theories.

	Beyond illuminating the logical structure of computer programs,
these results have some practical significance.  First, the correctness of
a computer program often involves facts about other mathematical domains,
2.5 these are often conveniently expressed in first order logic or in a
set theory axiomatized in first order logic.  It has proved particularly
difficult to work within logics that admit only continuous functions and
predicates.  Second, proof-checking and theorem proving programs have been
developed for first order logic.  Finally, first order logic is complete,
so that the Goedelian incompleteness of any theory is in the set of
axioms and can be reduced when necessary by additional axioms rather
than changing the logical system.

	While our goal is first order representations of recursive
programs, we will make considerable informal use of higher order
functionals and predicates.

	We present two methods of representing recursive programs.
The first involves a %2functional equation%1 and a %2minimization schema%1
for each program.
The functional equation has the function on both sides of an equality sign
and so defines it implicitly.
However, all variables are universally quantified.
The second approach defines the function explicitly, but existential quantifiers
asserting the existence of finite approximations to the function occur
in the formula.
The fact that the functional equation of a program not known to terminate
can nevertheless be written so simply
in first order logic was first discovered by Cartwright (1977), but the
remaining results seem to be new.


.bb "#. Recursive Programs."

	An adequate background for this paper is contained in (Manna 1974)
and more concisely in (Manna, Ness and Vuillemin 1973).  The connections
of recursive programs with second order logic are given in (Cooper 1969)
and (Park 1970).

	We shall consider mainly %2recursive programs%1 of the general form

!!g1:	%2f(x) ← %At%*[f](x)%1,

where %At%* is a %2computable functional%1 like

!!g2:	%2%At%* = λf.λx.(qif x = 0 qthen 1 qelse x . f(x - 1))%1,

which gives rise to the well known recursive definition of the factorial
function, namely

!!g3:	%2n! = qif n = 0 qthen 1 qelse n . (n - 1)!%1.

	In general, we shall be interested in partial functions from a
domain D1 to a domain D2, and it will often be necessary to augment these
domains by an undefined element denoted by %Aw%* giving rise to domains D1%5+%*
and D2%5+%*.  A set ⊗F of total base functions on the domains is assumed
available, and we study functions %2computable in the set F%1. 

	It is important to distinguish between a program as a text
and the partial function defined by the program
when one is interested in describing the dependence of the function on
the interpretation of the basic function and predicate symbols.  However,
we will be working with just one interpretation at a time, so we won't use
separate symbols for programs and the functions they define.
.bb "#. The Functional Equation of a Recursive Program."

	Consider the Lisp program

!!h1:	%2subst(x,y,z) ← qif qat z qthen (qif z=y qthen x qelse z)
qelse subst(x,y,qa z) . subst(x,y,qd z)%1.

The above is in Lisp %2external%1 or %2publication%1 notation in
which _qa_%2x%1_ (bold face qa) stands for %2car[x]%1,
_qd_%2x%1_ for %2cdr[x]%1, _%2x_._y%1_
for %2cons[x,y]%1, _qat_%2x%1_ for %2atom[x]%1, _qn_%2x%1_ for %2null[x]%1, and
%2<x%41%2 ... x%4n%1) for %2list[x%41%2, ... ,x%4n%1], and
%2x_*_y%1 for %2append[x,y]%1.  The program is written

	(DE SUBST (X Y Z) (COND ((ATOM Z) (COND ((EQUAL Z Y) X) (T Z)))
(T (CONS (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))

in Lisp %2internal notation%1.

	The basic functions α{%2car, cdr, cons, atomα}%1 of Lisp are all
assumed total, but we will say nothing about the values of ⊗car and
⊗cdr when applied to atoms.  According to the fixed point theory of
recursive programs, this program defines a function from ⊗Sexp (the
set of S-expressions) to Sexp%5+%* (the set of S-expressions augmented
by %Aw%*).  This function can be computed by any %2safe computation rule%1,
(in the terminology of Manna, Ness, and Vuillemin (1973)),
and when the computation terminates, its value will belong to ⊗Sexp.  When
the computation doesn't terminate, the value of ⊗f(x) is %Aw%*.  While
the particular function %2subst%1 always terminates, we do not assume it
in writing our first order formula.  Indeed we can use the first order
formula to prove by structural induction that %2subst%1 is total.

	These facts show that the function %2subst%1 defined recursively
by ({eq h1}) satisfies the sentence

!!h2:	%2∀x y z.(subst(x,y,z) = qif qat z qthen (qif z = y qthen x qelse z)
qelse subst(x,y,qa z) . subst(x,y,qd z))%1

of first order logic.  The variables %2x, y%1 and %2z%1 range over ⊗Sexp; 
when we want to quantify over %2Sexp%5+%1, we use %2X, Y %1and%2 Z%1.
Moreover, we are augmenting first order logic
(as described in (Manna 1975))
by allowing conditional
expressions as terms.  The augmentation is inessential, because
conditional expressions can always be eliminated from sentences by
distributing predicates over them.  Thus ({eq h2}) can be written

!!h3:	%2∀x y z.(qat z ⊃ (z=y ⊃ subst(x,y,z) = x) ∧ z≠y ⊃ subst(x,y,z) = z)
∧ ¬qat z ⊃ subst(x,y,z) = subst(x,y,qa z) . subst(x,y,qd z)),%1

but the conditional expression is clearer and closer to the program.

	A goal of our first order representation would be to use ({eq h1})
only to justify writing ({eq h2}) (or ({eq h3}) if you don't like
conditional expressions in the logic) and then prove all properties
of %2subst%1 using a first order axiomatization of Lisp.
.skip 2

.bb "#. First Order Axioms for Lisp."

	We use lower case variables ⊗x, ⊗y, and ⊗z with or without
subscripts to range over S-expressions.  Capitalized variables
range over all entities.  We also use variables ⊗u, ⊗v and ⊗w with
or without subscripts to range over lists, i.e. S-expressions
such that successive %2cdr%1s eventually reach NIL.  (The %2car%1 of
a list is not required to be a list).  We use predicates %2issexp%1
and %2islist%1 to assert that an individual is an S-expression or
a list.  First come the "housekeeping" and "algebraic" axioms:

L1:	%2∀x.issexp x%1

L2:	%2∀u.islist u%1

L3:	%2∀u.issexp u%1

L4:	%2¬issexp %Aw%1

L5:	%2islist %1NIL

L6:	%2qat qNIL%1

L7:	%2∀u.(qat u ⊃ u = qnil)%1

L8:	%2∀x y.issexp (x.y)%1

L9:	%2∀x u.islist (x.u)%1

L10:	%2∀x. ¬qat x ⊃ issexp qa x%1

L11:	%2∀x. ¬qat x ⊃ issexp qd x%1

L12:	%2∀u. u ≠ qNIL ⊃ islist qd u%1

L13:	%2∀x y. qa (x.y) = x%1

L14:	%2∀x y. qd (x.y) = y%1

L15:	%2∀x y. ¬qat (x.y)%1

L16:	%2∀x.¬qat x ⊃ (qa x . qd x) = x%1

	Next we have axiom schemata of induction

LS1:	%2(∀x.qat x ⊃ %AF%* x) ∧ ∀x.(¬qat x ∧ %AF%* qa x ∧ %AF%* qd x ⊃ %AF%* x) ⊃ ∀x.%AF%* x%1

LS2:	%2(∀u.u = qnil ⊃ %AF%* u) ∧ ∀u.(u ≠ qnil ∧ %AF%* qd u ⊃ %AF%* u) ⊃ ∀u. %AF%* u%1.

	From these axioms and schemata, we can prove

!!h4:	%2∀x y z.issexp subst(x,y,z)%1

which is our way of saying that %2subst%1 is total.
The key step is applying the axiom schema LS1 with the
predicate %2%AF%*(z) ≡ issexp(x,y,z)%1.
We can also prove
in first order logic
such algebraic properties of %2subst%1 as

!!h5:	%2∀x y z y1 z1.(¬occur(y,z1) ⊃ subst(subst(x,y,z),y1,z1) =
subst(x,y,subst(z,y1,z1)))%1

if we have suitable axiomatization of the predicate %2occur(x,y)%1 meaning
that the atom ⊗x occurs in the S-expression ⊗y. 

	The axiomatization of the predicate %2occur%1 raises some new
problems.  It is defined by the recursive Lisp program

!!h6:	%2occur(x,y) ← (x = y) ∨ (¬qat y ∧ (occur(x,qa y) ∨ occur(x,qd y)))%1.

If we were sure in advance that %2occur%1 were total, we could translate
the recursion ({eq h6}) into the sentence

!!h7:	%2∀x y.(occur(x,y) ≡
(x = y) ∨ (¬qat y ∧ (occur(x,qa y) ∨ occur(x,qd y))))%1

which will suffice for proving ({eq h5}), but we
have no right to write it down from the recursive definition ({eq h6}).

	What we are permitted to write is the implicit definition

!!h8:	%2∀x y.(occura(x,y) =
(x equals y) or (not atom y and (occura(x,qa y) or occura(x,qd y))))%1

and

!!h9:	%2∀x y.(occur(x,y) ≡ (occura(x,y) = T))%1

from which ({eq h7}) can eventually be proved in first order logic.

	Since recursive definitions give rise to partial predicates,
and we don't want to use a partial predicate logic, we introduce a domain
%AP%1 of %2extended truth values%1 with characteristic predicate %2isetv%1
whose elements are ⊗T, ⊗F and %Aw%*.
There is no harm in identifying ⊗T and ⊗F with suitable Lisp atoms or
with the integers 1 and 0.
The following axioms describe
functions into or out of %AP%2.

B1:	%2∀p.(isetv p)%1

B2:	%2∀p.(p = T ∨ p = F ∨ p = %Aw%2)%1

B3:	%2T ≠ F ∧ T ≠ %Aw%* ∧ F ≠ %Aw%1

B4:	%2∀p. isetv not p%1

B5:	%2∀p q. isetv(p and q)%1

B6:	%2∀p q. isetv(p or q)%1

B7:	%2∀p.(not p =
qif (p = %Aw%*) qthen %Aw%* qelse qif p = T qthen F qelse T)%1

B8:	%2∀p q.(p and q =
qif (p = %Aw%*) qthen %Aw%* qelse qif p = T qthen q qelse F)%1

B9:	%2∀p q.(p or q =
(qif p = %Aw%*) qthen %Aw%* qelse qif p = T qthen T qelse q)%1

B10:	%2∀X Y.(X equal Y = qif ¬issexp X ∨ ¬issexp Y qthen %Aw%* qelse qif
X = Y qthen T qelse F)%1

B11:	%2∀X.(aatom X =
qif ¬issexp X qthen %Aw%* qelse qif qat X qthen T qelse F)%1,

and we also need a conditional expression that can take an argument from %AP%1,
namely

B12:	%2∀p X Y.(if(p,X,Y) = qif p = %Aw%* qthen %Aw%* qelse qif p = T qthen X
qelse Y)%1.

	%2occura%1 is proved total by applying schema LS1 with
%2%AF%*(y) ≡ occura(x,y) ≠ %Aw%*%1.  After this %2occur%1 can be shown to
satisfy ({eq h7}).

	The axioms L1-L16 and B1-B12 together with the sentences arising
from the schemata LS1 and LS2 will be called the axiom system Lisp0.  We
will adjoin one more axiom later to get the system Lisp1.

	The above method of replacing a recursion by a first order
sentence was first (I think) used in (Cartwright 1977).  I'm
surprised that it wasn't invented sooner.

.skip 1
.indent 0,0;
.bb "#. The Minimization Schema."

	The functional equation of a program doesn't completely
characterize it.  For example, the program

!!h9a:	%2f1 x ← f1 x%1

leads to the sentence

!!h10:	%2∀x.(f1 x = f1 x)%1

which provides no information although the function ⊗f 
is undefined for all ⊗x.  This is not always the case, since
the program

!!h11:	%2f2 x ← (f2 x).qnil%1

has the functional equation

!!h12:	%2∀x.(f2 x = (f2 x).qnil)%1.

from which %2∀x.¬issexp f2(x)%1 can be proved by induction.

	In order to characterize recursive programs, we need some
way of asking for the least defined solution of the functional equation.

	Suppose the program is

!!h13:	%2f x ← %At%*[f](x)%1

yielding the functional equation

!!h14:	%2∀x.(f x = %At%*[f](x)%1.

The %2minimization schema%1 is then

!!h15:	%2∀x.(isD %At%*[%Af%*](x) ⊃ %Af%* x = %At%*[%Af%*](x)) ⊃ ∀x.(isD f x ⊃ %Af%* x = f x)%1.

	In the %2subst%1 example, the schema is

!!h16:	%2∀x y z.(issexp (qif qat z qthen (qif z = y qthen x qelse z)
qelse %Af%*(x,y,qa z).%Af%*(x,y,qd z)) ⊃ (%Af%*(x,y,z) = qif qat z qthen
(qif z = y qthen x qelse z) qelse %Af%*(x,y,qa z).%Af%*(x,y,qd z))) ⊃
∀x y z.(issexp subst(x,y,z) ⊃ %Af%*(x,y,z) = subst(x,y,z))%1.

	In the schema %Af%* is a free function variable of the appropriate
number of arguments.  The schema is just a translation into first order
logic of Park's (1970) theorem

!!h17:	%2%Af%* %8d%2 %At%*[%Af%*] ⊃ %Af%* %8d%2 Y[%At%*]%1.

	The simplest application of the schema is to show that the ⊗f1 
defined by ({eq h9a}) is never an S-expression.  The schema becomes

!!h18:	%2∀x.(issexp %Af%* x ⊃ %Af%* x = %Af%* x) ⊃ ∀x.(issexp f1 x ⊃ %Af%* x = f1 x)%1,

and we take

!!h19:	%2%Af%* x = %Aw%*%1.

The left side of ({eq h18}) is identically true, and, remembering that %Aw%*
is not an S-expression, the right side tells us that %2f1 x%1 is never
an S-expression.

	The minimization schema can sometimes be used to show partial
correctness.  For example, the well known 91-function is defined by
the recursive program over the integers

!!h20:	%2f91 x ← qif x > 100 qthen x - 10 qelse f91 f91(x + 11)%1.

The goal is to show that

!!h22:	%2∀x.(f91 x = qif x > 100 qthen 91 qelse 91%1.

We apply the minimization schema with

!!h21:	%2%Af%* x ← qif x > 100 qthen x - 10 qelse 91%1,

and it can be shown by an explicit calculation without induction that
the premiss of the schema is satisfied, and this shows that ⊗f91, 
whenever defined has the desired value.

	The method of recursion induction (McCarthy 1963) is also
an immediate application of the minimization schema.  If we show
that two functions satisfy the schema of a recursive program, we
show that they both equal the function computed by the program on
whereever the function is defined.

	The utility of the minimization schema for proving partial
correctness or non-termination depends on our ability to name
suitable comparison functions.  f1 and f91 were easily treated,
because the necessary comparison functions could be given explicitly
without recursion.  Any extension of the language that provides new
tools for naming comparison functions, e.g. going to higher order
logic, will improve our ability to use the schema in proofs.

	({eq h15}) can be regarded as an axiom schema involving
a second order function variable %At%1.  What can be substituted
for %At%1 is a  quantifier free
λ-expression in a first order function variable.
It may be interesting to study the sets of first order sentences that
can be generated by such second order sentence schemata.  Presumably,
sets of sentences can be generated in this way that cannnot be
generated by schemata with only first order function variables.
.skip 1
.bb "#. Proof Methods as Axiom Schemata"

	Representing recursive definitions in first order logic permits
us to express some well known methods for proving partial correctness
as axiom schemata of first order logic.

	For example, suppose we want to prove that if the input ⊗x of a
function ⊗f defined by

!!c1:	%2f x ← qif p x qthen x qelse f h x%1

satisfies %2%AF%2(x)%1, then if the function terminates, the output %2f(x)%1
will satisfy %AY%2(f(x))%1.  We appeal to the following %2axiom schema of
inductive assertions%1:

!!c2:	%2∀x.(%AF%2(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ qif p x qthen %AY%2(x,y)
qelse q(x,%8 %2h y))
.nofill
		⊃ ∀x.(%AF%2(x) ∧ inrange f x ⊃ %AY%2(x,f x))%1

.fill
where %2inrange f x%1 is the assertion that %2f(x)%1 is in the nominal
range of the function definition, i.e. is an integer or an S-expression
as the case may be, and asserts that the computation terminates.
In order to use the schema, we must invent a suitable predicate %2q(x,y)%1,
and this is precisely the method of inductive assertions.
The schema is valid for all predicates %AF%1, %AY%1, and %2q%1, and a
similar schema can be written for any collection of mutually recursive
definitions that is iterative.

	The method of %2subgoal induction%1 for recursive programs
was introduced in
(Manna and Pnueli 1970), but they didn't give it a name.
Morris and Wegbreit (1977) name it and apply it to ordinary programs.
Unlike %2inductive assertions%1, it isn't
limited to iterative definitions.  Thus, for the
recursive program

!!c3:	%2f%45%2 x ← qif p x qthen h x qelse g1 f%45%2 g2 x%1,

where ⊗p is assumed total, we have

!!c4:	%2∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧
∀x.(%AF%2(x) ∧ q(x,z) ⊃ %AY%2(x,z))
.nofill
		⊃ ∀x.(%AF%2(x) ∧ inrange(f(x)) ⊃ %AY%2(x,f(x)))%1
.fill

	We can express these methods as axiom schemata,
because we have the predicate %2inrange%1 to express termination.
The minimization schema itself can be proved by subgoal induction.
We need only take %2%AF%2(x)_≡_%3true%1 and %AY%2(x,y)_≡_(y_=_%Af%2(x))%1
and %2q(x,y)_≡_(y_=_%Af%2(x))%1.

	We have not given a general rule for going from the recursive
definition (or equivalently from the functional equation and minimization
schema) to the schema of subgoal induction.
A suitable rule is given in
(Manna and Pnueli 1970); we need only add a conclusion involving
the %2inrange%1 predicate to their formula %2W%4P%1.
It doesn't seem to be a schema in %At%1.

.skip 2
.bb "#. Representations Using Finite Approximations."

	Our second approach to representing recursive programs
by first order formulas goes back to Goedel (1931, 1934) who showed
that primitive recursive functions could be so represented.  (Our
knowledge of Goedel's work comes from (Kleene 1951)).

.turn on "α"
.eq←0
	Kleene (1951) calls a function ⊗f %2representable%1 if there
is an arithmetic formula ⊗A with free variables ⊗x and ⊗y such
that

!!b1:	%2∀x_y.((y_=_f(x))_≡_A)%1,

where an arithmetic formula is built up from integer constants and
variables using only addition, multiplication and bounded quantification.
Kleene showed that all partial recursive functions are representable.
The proof involves Goedel numbering possible computation sequences
and showing that the relation between sequences and their elements
and the steps of the computation are all representable.

	In Lisp less machinery has to be built up, because sequences
are Lisp data, and the relation between a sequence and its elements
is given by basic Lisp functions and by the %2subexpression relation%1
defined by

!!b2:	%2x subexp y ← (x = y) ∨ ¬qat y ∧ [x subexp qa y ∨ x subexp qd y]%1.

	%2subexp%1 is the only recursive definition we shall require.
Since it is total, we only need its functional equation to represent
it in first order logic.  The functional equation is

L17:	%2∀x y.(x subexp y ≡ (x=y) ∨ ¬qat y ∧ (x subexp qa y ∨ x subexp qd y))%1,

	The axiom system consisting of L1-L17, B1-B12, and the sentences
resulting from the schemata LS1 and LS2 will be called the axiom system
Lisp1.

	Starting with %2subexp%1 and the basic Lisp functions and
predicates we will define three other Lisp predicates without recursion.
By %2u_istail_v%1 we mean that ⊗u can be obtained from ⊗v by repeated
%2cdr%1s.  Thus the tails of (A B C D) are (A B C D), (B C D), (C D),
(D) and NIL.  The natural recursive definition of %2istail%1 is

!!b3a:	%2u istail v ← (u = v) ∨ (¬qn v ∧ u istail qd v)%1

which according to the previous sections would lead to the first order
formula

!!b3b:	%2∀u v.(u istail v ≡ (u = v) ∨ (¬qn v ∧ u istail qd v))%1,

but ({eq b3b}) is still an implicit definition of %2istail%1, because
the function being defined occurs on both sides of the equivalence
sign.  A suitable explicit definition is

!!b3:	%2∀u v.(u istail v ≡ u subexp v ∧ ∀x.(u subexp x ∧ x subexp v
⊃ x = u ∨ u subexp qd x))%1.

Next we shall define membership in a list.  We have

!!b4:	%2∀x v.(x ε v ≡ ∃u.(u istail v ∧ x = qa u))%1.

Now we define an %2a-list%1 - a familiar Lisp concept.  We have

!!b5:	%2∀w.(isalist w ≡ ∀x.(x ε w ⊃ ¬qat x) ∧ ∀x1 x2.(x1 ε w ∧
x2 ε w ∧ qa x1 = qa x2 ⊃ x1 = x2))%1.

Thus an %2a-list%1 is a list of pairs such that no S-expression is the
first element of two different pairs.  Therefore, a-lists are suitable for
representing finite lists of argument-value pairs for partial functions.

	Finally, we need the familiar Lisp function %2assoc%1 that is used
for looking up atoms on %2a-lists%1.  Its recursive definition
is

!!b6:	%2assoc(x,w) ← qif qn w qthen qnil qelse qif x = qaa w qthen qa w
qelse assoc(x,qd w)%1,

which can be represented by

!!b7:	%2∀w x y.(x.y = assoc(x,w) ≡ ∃w1.(w1 istail w ∧ x.y = qa w1)
∨ assoc(x,w) = qnil)%1.

	Now let ⊗f be defined recursively by

!!b8:	%2f x ← %At%*[f](x)%1.

In order to emphasize the parallel between a partial function %2f%1 and
an %2a-list%1 used as a finite approximation, we define

!!b8a:	%At%2'(w)(x) = %At%2[λz.qif qn assoc(z,w) qthen %Aw%2
qelse qd assoc(z,w)](x)%1.

Thus %At%1' is like %At%1 except that whenever %At%1 evaluates its functional
argument ⊗f at some value ⊗z, %At%1' looks up ⊗z on the a-list ⊗w. 

	With this preparation we can write

!!b9:	%2∀x y.(y = f(x) ≡ ∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = %At%2'[qd w1](x1))) ∨ f(x) = %Aw%2)%1.

	The essence of this formula is simple.  ⊗w is an a-list
containing all argument-value pairs that arise in the evaluation of ⊗f(x). 
We require that if ⊗x occurs somewhere on ⊗w, the pairs involved in the
evaluation of ⊗f(x) occur further on in the a-list ⊗w.  This is to avoid
allowing circular recursions.  If there is no such a-list, then
%2f(x)_=_%Aw%1.

	If the logic has a description operator %Ai%1, where
%Ai%2 x.P(x)%1 stands for the "the unique ⊗x such that ⊗P(x) if
there is such a unique ⊗x and otherwise %Aw%1", then ({eq b9}) can
be written

!!b9a:	%2∀x.(f(x) = %Ai%2 y.∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = %At%2'[qd w1](x1))))%1.

	As an example, consider the Lisp function %2ff%1 defined
recursively by

!!b10:	%2ff x ← qif qat x qthen x qelse ff qa x%1.

({eq b9a}) then takes the form

!!b11:	∀x.(ff x = %Ai%2y.∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = qif qat x1 qthen x1 qelse (qif qn assoc(x1,qd w1)
qthen %Aw%2 qelse qd assoc(x1,qd w1)))))%1.

	Suppose we were computing %2ff_((A.B).C)%1.  A suitable ⊗w would
be ((((A.B).C).A) ((A.B).A) (A.A)).

	It might be asked whether %2subexp%1 is necessary.  Couldn't we
represent recursive programs using just %2car, cdr, cons%1 and %2atom%1?
No, because the any sentence involving just these functions is decideable,
because any such sentence can be converted to an equivalent sentence in the pure
theory of equality.

	In case of functions of several variables,
({eq b9}) corresponds to a call-by-value
computation rule while the representations of the previous sections correspond
to call-by-name or other "safe" rules.
.BB "#. Questions of Incompleteness."

	Luckham, Park and Paterson (1970) have shown that whether a
program schema diverges for every interpretation, whether it diverges
for some interpretation, and whether two program schemas are equivalent
are all not even partially solvable problems.  Manna (1974) has a
thorough discussion of these points.  In view of these results, what
can be expected from our first order representations?

	First let us construct a Lisp computation that does not terminate,
but whose non-termination cannot be proved from the axioms Lisp1 within
first order logic.  We need only program a proof-checker for first order
logic, set it to generate all possible proofs starting with the axioms Lisp1,
and stop when it finds a proof of (qnil ≠ qnil) or some other contradiction.
Assuming the axioms are consistent, the program will never find such a
proof and will never stop.  In fact, proving that the program will never
stop is precisely proving that the axioms are consistent.  But Goedel's
theorem asserts that axiom systems like Lisp1 cannot be proved consistent
within themselves.
All the known cases of terminating computations that
can't be proved not to terminate within Peano arithemtic
involve such an appeal to Goedel's theorem
or to similar unsolvability arguments.

	We can presumably prove Lisp1 consistent
just as Gentzen proved arithmetic consistent - at the price of introducing
a new axiom schema that allows induction up to the transfinite ordinal
ε%40%1.  Proving the new system consistent will require induction up to
a still higher ordinal, etc.

	Since every recursively defined function can be defined explicitly,
any sentence involving such functions can be replaced by an equivalent
sentence involving only %2subexp%1 and the basic Lisp functions.
The theory of subexp and these functions has a standard model, the
usual S-expressions and many non-standard models.  We "construct"
non-standard models in the usual way by appealing to the theorem that
if every finite subset of a set ⊗S of sentences of first order logic
has a model, then ⊗S has a model.
For example, take %2S = α{qnil subexp x, %1(A)%2 subexp x, %1(A A)%2
subexp x, ...%1 indefinitelyα}.  Every finite subset of ⊗S has a model;
we need only take ⊗x to be the longest list of A's occurring in the
sentences.
Hence there is a model of the Lisp axioms in which ⊗x has all lists
of A's as subexpressions.  No sentence true in the standard model
and false in such a model can be proved from the axioms.  However,
it is necessary to be careful about the meaning of termination of a
function.  In fact, taking successive %2cdr%1s of such an ⊗x would
never terminate, but the sentence whose %2standard interpretation%1
is termination of the computation is provable from Lisp1.

	The practical question is: where does the correctness of ordinary
programs come in?  It seems likely that such statements will be provable
with our original system of axioms.  It doesn't follow that the system
Lisp1 will permit convenient proofs, but probably it will.  The heuristic
evidence for this comes from (Cohen 1965).  Cohen presents two systems
of axiomatized arithmetic Z1 and Z2.  Z1 is ordinary Peano arithmetic with
an axiom schema of induction, and Z2 is an axiomatization of hereditarily
finite sets of integers.  Superficially, Z2 is more powerful than Z1, but
because the set operations of Z2 can be represented in Z1 as functions
on the Goedel numbers of the sets, it turns out that Z1 is just as powerful
once the necessary machinery has been established.  Because sets and lists
are the basic data of Lisp1, and sets are easily represented, the power of Lisp1
will be approximately that of Z2, and convenient proofs of correctness
statements should be possible.  It would be nice to be able to express these
considerations less vaguely.
.bb "#. References."

%3Cartwright, R.S. (1977)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cohen, Paul (1966)%1: %2Set Theory and the Continuum Hypothesis%1,
W.A. Benjamin Inc.

%3Cooper, D.C. (1969)%1: "Program Scheme Equivalences and Second-order
Logic", in B. Meltzer and D. Michie (eds.), %2Machine Intelligence%1,
Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.

%3Kleene, S.C. (1951)%1: %2Introduction to Metamathematics%1,
Van Nostrand, New York.

%3Luckham, D.C., D.M.R.Park, and M.S. Paterson (1970)%1: "On Formalized
Computer Programs", %2J. CSS%1, %34%1(3): 220-249 (June).

%3Manna, Zohar and Amir Pnueli (1970)%1: "Formalization of the Properties
of Functional Programs", %2J. ACM%1, %317%1(3): 555-569.

%3Manna, Zohar (1974)%1: %2Mathematical Theory of Computation%1,
McGraw-Hill.

%3Manna, Zohar, Stephen Ness and Jean Vuillemin (1973)%1: "Inductive Methods
for Proving Properties of Programs", %2Comm. ACM%1,%316%1(8): 491-502 (August).

%3Morris, James H., and Ben Wegbreit (1977)%1: "Program Verification
by Subgoal Induction", to appear.

%3Park, David (1969)%1: Fixpoint Induction and Proofs of Program
Properties", in %2Machine Intelligence 5%1, pp. 59-78, Edinburgh
University Press, Edinburgh.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
FIRST.NEW[W77,JMC]
PUBbed at {time} on {date}.%1